ds:x:Id fp Type, da:k:Knd fp Type, i:Id, es:ES.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 (e1, e2:E.
 (loc(e1) = i
 ( loc(e2) = i
 ( (t:event-info(ds;da). (t  es-hist{i:l}(es;e1;e2))  e[e1,e2].t = es-info(es;e))) 

latex

Definitions	t  T, x:A. B(x), loc(e), Id, E, b, P  Q, False, A, es-info(es;e), event-info(ds;da), Prop, x. t(x), e[e1,e2].P(e), (x  l), P  Q, es-hist{i:l}(es;e1;e2), P & Q, P  Q, a:A fp B(a), Knd, ES, Top, IdDeq, f(x)?z, vartype(i;x), kind(e), KindDeq, valtype(e), [e, e'], {T}, SQType(T), x:A. B(x), e  e' , A & B, ||as||, AB, , True, T, l[i], ij
Lemmas	length wf1, select wf, squash wf, true wf, member-es-interval, es-le wf, es-le-loc, member map, Id sq, es-interval wf2, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, Knd wf, fpf wf, l member wf, es-hist wf, l member subtype, existse-between2 wf, event-info wf, es-info wf, es-loc-pred, es-E wf, Id wf, es-loc wf